A:Type, es:ES, I:AbsInterface(A), P:(E), p:(e:E. Dec(P(e))).
((I|p)|p) = (I|p)  AbsInterface(A) 

latex

Definitions	x:A. B(x), f(a), x(s), (I|p), e  X, t  T, b, P  Q, E, x.A(x), x. t(x), Type, ES, AbsInterface(A), , x:AB(x), Dec(P), <a, b>, s = t, P & Q, x:A  B(x), P  Q
Lemmas	es-is-interface-restrict, decidable wf, es-E wf, es-interface wf, event system wf, es-interface-restrict-trivial, es-interface-restrict wf, assert wf, es-is-interface wf